<html>
<head><meta charset="utf-8"><title>Reading suggestions · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html">Reading suggestions</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="203695360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203695360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Teymour Aldridge <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203695360">(Jul 13 2020 at 09:44)</a>:</h4>
<p>Does anyone have any reading suggestions for theory on formal verification? I'm after something introductory.<br>
Apologies if this isn't the right stream to ask in – if it isn't I'd be grateful if someone could suggest where the correct place to ask this would be.</p>



<a name="203695412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203695412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203695412">(Jul 13 2020 at 09:44)</a>:</h4>
<p>what's your background? is there anything in specific you're interested in?</p>



<a name="203695575"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203695575" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Teymour Aldridge <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203695575">(Jul 13 2020 at 09:46)</a>:</h4>
<p>I don't really have a background in anything specific – I have some general computer science knowledge though. I'm interested in formal verification (proving that programs work as intended) of software programs – something that would allow me to understand Prusti's codebase (it's a "prototype verifier" built on Viper) would be useful.</p>



<a name="203696876"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203696876" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203696876">(Jul 13 2020 at 10:02)</a>:</h4>
<p>To understand Prusti's internals a necessary step is to learn about <a href="https://www.pm.inf.ethz.ch/research/viper.html">Viper</a>. That page links to several papers, but the <a href="http://viper.ethz.ch/tutorial/">tutorial</a> is probably the best starting place. If you are looking for a broader introduction to formal software verification, I would suggest to look for lecture slides or recordings on Google. For example, <a href="https://www.pm.inf.ethz.ch/education/courses/program-verification.html">this course at ETH</a> explains how Viper is realized.</p>



<a name="203696920"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203696920" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203696920">(Jul 13 2020 at 10:03)</a>:</h4>
<p>you can also look at this course from the MPRI <a href="https://www.lri.fr/~marche/MPRI-2-36-1/">https://www.lri.fr/~marche/MPRI-2-36-1/</a> for a general introduction to deductive verification</p>



<a name="203700246"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203700246" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Teymour Aldridge <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203700246">(Jul 13 2020 at 10:46)</a>:</h4>
<p>Thanks a lot for these recommendations! These look interesting. I'll have a look at the suggested courses (and search DuckDuckGo for some more).</p>



<a name="203702179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203702179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203702179">(Jul 13 2020 at 11:11)</a>:</h4>
<p>also ask questions here!! I want to revive this channel as much as possible</p>



<a name="203702222"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203702222" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203702222">(Jul 13 2020 at 11:12)</a>:</h4>
<p>I have this tab pinned so it's nearly always open for me</p>



<a name="203702455"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Reading%20suggestions/near/203702455" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Teymour Aldridge <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Reading.20suggestions.html#203702455">(Jul 13 2020 at 11:15)</a>:</h4>
<p>Thanks for the offer! I'll try and join in on the revival of the formal methods channel.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>